$\forall$$R$:es\_realizer\{i:l\}, $i$:Id. \\[0ex]($\neg$($\uparrow$Rplus?($R$))) $\Rightarrow$ ($\neg$($\uparrow$Rnone?($R$))) $\Rightarrow$ (R{-}has{-}loc($R$; $i$) = eq\_id(R{-}loc($R$); $i$) $\in$ $\mathbb{B}$)